﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using TruthTree2.FOL.Logic;

namespace TruthTree2.FOL.Resolution
{
    public class Clause
    {
        internal Literal[] atoms;
        internal int arity { get { return atoms.Length; } }

        public Clause(params Literal[] a)
        {
            atoms = removeUnneeded(a);
            Array.Sort(atoms);
        }

        private bool containsUnifiableLiterals(Clause c, out Literal la, out Literal lb)
        {
            foreach (Literal a in atoms)
            {
                foreach (Literal b in c.atoms)
                {
                    if(a.IsSamePredicateNegated(b))
                    {
                        la = a;
                        lb = b;
                        return true;
                    }
                    else if (a.atom is Identity)
                    {
                        Identity i = (Identity)a.atom;
                        if (b.atom.ContainsTerm(i.left) || b.atom.ContainsTerm(i.right))
                        {
                            la = a;
                            lb = b;
                            return true;
                        }
                    }
                    else if (b.atom is Identity)
                    {
                        Identity i = (Identity)b.atom;
                        if (a.atom.ContainsTerm(i.left) || a.atom.ContainsTerm(i.right))
                        {
                            la = a;
                            lb = b;
                            return true;
                        }
                    }
                }
            }

            la = null;
            lb = null;
            return false;
        }

        public bool Unify(Clause c, out Clause res)
        {
            Literal preda;
            Literal predb;
            res = null;
            if (containsUnifiableLiterals(c, out preda, out predb))
            {
                Dictionary<Term, Term> binding;
                int ident = (preda.atom is Identity ? 1 : (predb.atom is Identity ? 2 : 0));
                if (preda.Unify(predb, out binding))
                {
                    foreach (KeyValuePair<Term, Term> kvp in binding)
                    {
                        if (kvp.Value.ContainsTerm(kvp.Key)) { return false; }
                    }

                    List<Literal> unified = new List<Literal>();
                    foreach (Literal a in atoms) { if (ident != 1 || !preda.Equals(a)) { unified.Add(a.Rename(binding)); } }
                    foreach (Literal a in c.atoms) { if (ident != 2 || !predb.Equals(a)) { unified.Add(a.Rename(binding)); } }

                    res = new Clause(unified.ToArray());
                    return true;
                }
            }

            return false;
        }

        private Literal[] removeUnneeded(Literal[] at)
        {
            List<Literal> realatoms = new List<Literal>();
            for (int a = 0; a < at.Length; a++)
            {
                bool include = true;
                for (int b = 0; b < at.Length; b++)
                {
                    if (a == b) { continue; }
                    if (at[a].IsNegation(at[b])) { include = false; break; }
                }

                if (include) { realatoms.Add(at[a]); }
            }

            return realatoms.Distinct().ToArray();
        }

        public Clause Resolve(Clause o)
        {
            List<Literal> resolvents = new List<Literal>();
            resolvents.AddRange(atoms);
            resolvents.AddRange(o.atoms);

            return new Clause(resolvents.ToArray());
        }

        public override string ToString()
        {
            if (arity > 1)
            {
                return String.Format("{{{0}}}", String.Join<Literal>(", ", atoms));
            }

            return String.Join<Literal>(", ", atoms);
        }

        public override int GetHashCode()
        {
            return ToString().GetHashCode();
        }

        public override bool Equals(object obj)
        {
            if (obj is Clause)
            {
                Clause c = (Clause)obj;
                return ToString().Equals(c.ToString());
            }

            return false;
        }
    }
}
